Kiểm tra kiểu Hệ_thống_kiểu

Quán trình kểm tra và thực thi các ràng buộc của kiểu—kiểm tra kiểu (type checking)— có thể xảy ra ở thời gian biên dịch (kiểm tra tĩnh) hoặc thời gian chạy. Nếu một đặc tả ngôn ngữ yêu cầu các quy tắc kiểu mạnh (ví dụ, chỉ cho phép ít hay nhiều việc chuyển đổi kiểu tự động mà không làm mất thông tin), quá trình đó gọi là kiểu mạnh, còn không, gọi là kiểu yếu. Các thuật ngữ này thường không được dùng theo nghĩa chặt chẽ.

Kiểm tra kiểu tĩnh

Kiểm tra kiểu tĩnh (static type checking) là quá trình xác minh an toàn kiểu của một chương trình dựa vào sự phân tích văn bản (mã nguồn) của chương trình. Nếu một chương trình vượt qua được bộ kiểm tra kiểu tĩnh, khi đó chương trình đảm bảo đáp ứng được một số đặc tính an toàn cho tất cả đầu vào.

Kiểm tra kiểu động và thông tin kiểu thời gian chạy

Kiểm tra kiểu động (dynamic type checking) là quá trình xác minh an toàn kiểu của chương trình vào thời gian chạy.

Kết hợp kiểm tra kiểu tĩnh và động

Một số ngôn ngữ cho phép cả kiểm tra kiểu tĩnh và động, đôi khi gọi là kiểm tra kiểu mềm (soft typing).

Kiểm tra kiểu tĩnh và động trong thực tế

Cần sự đánh đổi nhất định khi lựa chọn giữa kiểm tra kiểu tĩnh và động.

Hệ thống kiểu mạnh và kiểu yếu

An toàn kiểu và an toàn bộ nhớ

Bài chi tiết: An toàn kiểu

Các mức độ kiểm tra kiểu

Một số ngôn ngữ cho phép các mức độ kiểm tra kiểu khác nhau áp dụng cho từng vùng mã khác nhau.

Hệ thống kiểu tùy chọn

Nó được đề xuất chủ yếu bởi Gilad Bracha, cho phép lựa chọn hệ thống kiểu có thể độc lập với lựa chọn ngôn ngữ; như vậy một hệ thống kiểu nên là một mô đun để có thể gắn vào một ngôn ngữ khi cần.